Context

Before applying rewrites, we need a way to find matches. We are both interested in subgraph isomorphisms and generic morphisms. For example, in the Rewrite Theory papers, a match is not restricted to only embeds.

Details

• Morphism can be created only via find_homomorphisms and find_isomorphisms methods that guarantee that it is actually a morphism. We can use it as input for rewrite function in here Rewriting for Lax Hypergraphs #20 where we may relax assertions on the candidate match.
• There are many "pruning" strategies we can apply to reduce the state space blowup. I think we should find a compromise between code readability and "best effort". For big graphs or special cases, we might even considering using a specialized external solver.
• Note: matching is order sensitive for sources and targets, I think it is ok in our context. Why? Thinking in terms of graphs representing programs: the order in which I apply arguments usually matters. 0/7 != 7/0.
• The algorithm is a VF2‑inspired backtracking matcher, with optional injectivity. We don't use CSP because we want the algorithm to work in the particular case of hypegraphs.
• There are multiple pruning strategies that we can introduce, but at this stage, they sound more like over-engineering. So instead of optimizing the algorithm without having a clear target in mind, I preferred to add a way to trace the backtracking. This will help us profile the implementation for future optimizations.

Discussion

Note: here we talk about the match Pattern -> Host, not the left rule Interface -> Pattern.

In this implementation, a match is a generic morphism. As an option we can enforce mono on both nodes and edges. In many practical contexts, it makes sense to restrict to mono since we are interested in embeddings (e.g. matches on AST or IR). However, non-mono matches might be closer to Frobenius philosophy. For example, target f(a,a) where a is the same wire connected to two ports and rule is f(x,x) with two distinct wires with the same label.

In the literature, sometimes, mono matches are mono on nodes only. For graphs, it doesn't matter, but the difference is important for hypergraphs. However, in some cases, pattern hyperedges are identified solely by their node sets and label, so if two pattern hyperedges have the same nodes, they are considered the same hyperedge rather than distinct ones, thus mono on nodes automatically implies mono on hyperedges. If we are in this situation, we might think of relaxing the definition of match.

What definitions of "match" are used in other tools and literature? Warning: ChatGPT generated.

• DPO-based tools match is usually mono.
• Catlab.jl: homomorphisms by default; monic/injective optional (monic=true). Categorical generality (we instead focus only on hypergraphs); can emulate classical DPO matching by restricting to monics. They adapted CSP to ACSets.
• Quantomatic: effectively injective occurrence matching
• PyZX: not a generic match morphism API; uses rule-specific matchers that scan graph neighborhoods and pick non-overlapping rewrite sites.